chore(Data/Finsupp): make `mapDomain_congr` congr by YaelDillies · Pull Request #39575 · leanprover-community/mathlib4

YaelDillies · 2026-05-19T12:13:56Z

This makes simp stronger. It particular, it breaks some proofs that relied on simp being weak.

From MeanFourier

github-actions · 2026-05-19T12:15:04Z

PR summary f034c03164

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ coe_id
+ mapDomain_fun_comp

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f034c03164
Reference commit e780b56e92

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-merge-conflicts · 2026-07-04T15:12:00Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-07-08T22:15:01Z

This pull request has conflicts, please merge master and resolve them.

eric-wieser · 2026-07-15T13:05:16Z


 @[simp]
-theorem repr_reindex : (b.reindex e).repr x = (b.repr x).mapDomain e :=
+theorem repr_reindex : (b.reindex e).repr x = (b.repr x).equivMapDomain e :=


What motivated this?

This makes the simp set more confluent. Otherwise simp fails to prove reindexFinsetRange_repr because the new congr lemma allows it to simplify the inside of the expression further earlier

eric-wieser · 2026-07-15T13:39:05Z

+-- The linter complains that `mapDomain_id` can be proved from `mapDomain_fun_id` and `id_eq`
+-- but this isn't true (at least within most of mathlib)


Why isn't this true? It looks to me like the congr lemma would eta-expand id, which leads to that chain.

(I wonder if simp high would be more appropriate to silence the linter)

I already tried simp high and simp\d a while ago and neither worked to silence the linter.

Can you elaborate on "this isn't true (at least within most of mathlib)"?

@[to_fun mapDomain_fun_id] lemma mapDomain_id : mapDomain id v = v := sum_single _ /-- info: -- Found 0 errors in 41 declarations (plus 22 automatically generated ones) in the current file with 15 linters -- All linting checks passed! -/ #guard_msgs in #lint

but if I do it with import Mathlib, then it complains. I tried bisecting quickly and I seem to be able to import most of mathlib without complaining

Sorry, I misdiagnosed and you are perfectly right. simp\d does silence the linter as expected.

Let me be clearer; I think that perhaps this lemma should not be tagged simp at all, precisely for the reason that the linter says? What proofs break if this is not simp?

joneugster

Thanks, LGTM!

maintainer merge

github-actions · 2026-07-17T13:59:11Z

🚀 Pull request has been placed on the maintainer queue by joneugster.

Vierkantor · 2026-07-22T16:44:03Z

Any final comments from Eric?

bors d=@eric-wieser

mathlib-bors · 2026-07-22T16:44:05Z

✌️ eric-wieser can now approve this pull request until 2026-08-05 16:44 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

eric-wieser · 2026-07-22T16:49:41Z

I was hoping to look further at #39575 (comment) but haven't found the time yet.

YaelDillies · 2026-07-23T10:36:24Z

I was hoping to look further at #39575 (comment)

I just resolved this comment, so hopefully Eric is happy with it now?

github-actions Bot added the t-convex-geometry Affine geometry, cones, simplices label May 19, 2026

YaelDillies mentioned this pull request May 19, 2026

[Merged by Bors] - feat(Geometry/Convex): modules are convex spaces #39531

Closed

YaelDillies force-pushed the map_domain_congr branch 4 times, most recently from 8867e7c to 3899098 Compare May 21, 2026 10:54

YaelDillies added t-data Data (lists, quotients, numbers, etc) and removed t-convex-geometry Affine geometry, cones, simplices labels Jun 27, 2026

YaelDillies requested a review from eric-wieser June 28, 2026 12:04

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 4, 2026

YaelDillies force-pushed the map_domain_congr branch from 9a4c77d to 458cedf Compare July 4, 2026 16:03

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 4, 2026

mathlib-triage Bot assigned joneugster Jul 7, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 8, 2026

chore(Data/Finsupp): make mapDomain_congr congr

882c618

YaelDillies force-pushed the map_domain_congr branch from 1589a31 to 882c618 Compare July 9, 2026 07:53

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 9, 2026

YaelDillies mentioned this pull request Jul 15, 2026

feat: add DFinsupp.mapDomain to match Finsupp.mapDomain #38977

Open

1 task

eric-wieser reviewed Jul 15, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean Outdated

eric-wieser reviewed Jul 15, 2026

View reviewed changes

revert

2e474f6

eric-wieser reviewed Jul 15, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Intertwining.lean Outdated

simp high

70ae40e

joneugster approved these changes Jul 17, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 17, 2026

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 22, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 22, 2026

YaelDillies added 2 commits July 23, 2026 12:29

Merge remote-tracking branch 'origin/master' into map_domain_congr

13fb655

lint simpNF

f034c03

		-- The linter complains that `mapDomain_id` can be proved from `mapDomain_fun_id` and `id_eq`
		-- but this isn't true (at least within most of mathlib)

Uh oh!

Conversation

YaelDillies commented May 19, 2026

Uh oh!

github-actions Bot commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary f034c03164

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- pending)

Uh oh!

mathlib-merge-conflicts Bot commented Jul 4, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jul 8, 2026

Uh oh!

Uh oh!

eric-wieser Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 23, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jul 23, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Jul 17, 2026

Uh oh!

Vierkantor commented Jul 22, 2026

Uh oh!

mathlib-bors Bot commented Jul 22, 2026

Uh oh!

eric-wieser commented Jul 22, 2026

Uh oh!

YaelDillies commented Jul 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions Bot commented May 19, 2026 •

edited

Loading

eric-wieser Jul 15, 2026 •

edited

Loading

YaelDillies Jul 15, 2026 •

edited

Loading

YaelDillies Jul 15, 2026 •

edited

Loading

YaelDillies Jul 15, 2026 •

edited

Loading